M1, M2:MsgA. (M1 = M2)  M1  M2 

latex

Definitions	t  T, x:A. B(x), M1  M2, MsgA, s = t, , P  Q, FinProbSpace, Id, x.A(x), type List, IdLnk, Knd, product-deq(A;B;a;b), x:A  B(x), IdLnkDeq, Void, Type, x. t(x), t.2, rcv(l,tg), f(x)?z, Top, t.1, x:AB(x), State(ds), , , KindDeq, IdDeq, f  g, P & Q, A c B, Valtype(da;k)
Lemmas	fpf-sub weakening, Id wf, id-deq wf, Knd wf, Kind-deq wf, bool wf, rationals wf, IdLnk wf, ma-state wf, pi1 wf, top wf, fpf-cap wf, rcv wf, pi2 wf, idlnk-deq wf, product-deq wf, finite-prob-space wf, msga wf, ma-sub wf